﻿using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;

namespace Logic
{
	class Program
	{
		static void Main(string[] args)
		{
            //TestOnRandomCNF();

			

            while (true)
            {
                MinesHost host = new MinesHost(30, 16, 99);
                System.Threading.Thread.Sleep(100); //for random seeds to differ
                MinesAgent agent = new MinesAgent(host);

                while (true)
                {
                    Console.CursorLeft = Console.CursorTop = 0;
                    agent.Act();
                    if (agent.IsDead || agent.IsSolved) break;
                    
                    Console.WriteLine();
                    host.DrawField();
                    Console.WriteLine();
                    agent.DrawFacts();
                    //Console.ReadLine();
                }

                Console.CursorTop = Console.CursorLeft = 0;
                if (agent.IsDead)
                {
                    Console.ForegroundColor = ConsoleColor.DarkRed;
                    Console.WriteLine("Agent is dead. Try again.                       ");
                }
                else
                {
                    Console.ForegroundColor = ConsoleColor.Green;
                    Console.WriteLine("I'm done. [glasses on].                          ");
                }

                Console.ForegroundColor = ConsoleColor.Gray;
                Console.ReadLine();
            }
		}


        static void TestOnRandomCNF()
        {
            LogicalSystem testWorld = new LogicalSystem(Enumerable.Range(0, 50).Select(x => x.ToString()).ToArray());

            while (true)
            {
                Random rand = new Random();
                List<List<int>> formula = new List<List<int>>();
                for (int i = 0; i < 200; i++)
                {
                    List<int> clause = new List<int>();
                    for (int j = 0; j < 3; j++)
                    {
                        int v = rand.Next(testWorld.Symbols.Count);
                        if (rand.NextDouble() < 0.5)
                            v = ~v;
                        clause.Add(v);
                    }
                    formula.Add(clause);
                }

                CNFSentence test3CNF = new CNFSentence(testWorld, formula);
                var original = (CNFSentence)test3CNF.Clone();
                test3CNF.Compact();
                //if (!original.IsEquivalentTo(test3CNF)) throw new Exception();
                test3CNF.BuildIndex();

                SATSolver solv = new SATSolver();
                int[] res = solv.Solve(test3CNF);
                Console.WriteLine("Nodes: " + solv.NodesExpanded);


                if (res == null)
                    Console.WriteLine("No solution");
                else
                {
                    if (!solv.CheckSolution(test3CNF, res))
                    {
                        throw new Exception();
                    }

                    for (int i = 0; i < res.Length; i++)
                    {
                        Console.WriteLine(testWorld.Symbols[i] + " > " + (res[i] == 1 ? "True" : (res[i] == -1 ? "False" : "Any")));
                    }
                }

                Console.ReadLine();
            }
        }

		#region old test code
			//List<string> ws = new List<string>();
			//int size = 4;
			//for(int x = 1; x <= size; x++)
			//    for (int y = 1; y <= size; y++)
			//    {
			//        string index = x + "," + y;
			//        ws.Add("P" + index);
			//        ws.Add("W" + index);
			//        ws.Add("B" + index);
			//        ws.Add("S" + index);
			//    }
			//LogicalSystem wumpusWorld = new LogicalSystem(ws);


			////LogicalSystem testWorld = new LogicalSystem(new[] { "A", "B", "C", "D", "E", "F", "G", "H" });


			////Func<int[], bool> twoMines = x =>
			////    {
			////        int c = 0;
			////        for (int i = 0; i < 8; i++)
			////            if (x[i] == 1) c++;
			////        return c == 4;
			////    };



			////CNFSentence cnf;
			////while (true)
			////{
			////    cnf = CNFSentence.FromTruthTable(testWorld, twoMines, 8);
			////    var cnf2 = (CNFSentence)cnf.Clone();
			////    cnf.Compact();
			////    if (!cnf.IsEquivalentTo(cnf2)) throw new Exception();
			////    Console.WriteLine(cnf2);
			////    Console.WriteLine();
			////    Console.WriteLine(cnf);
			////    Console.ReadLine();

			////    #region CNF hybercube check
			////    int[] ass = new int[8];
			////    for (int i = 0; i < 8; i++)
			////        ass[i] = -1;
			////    int j = 0;

			////    for (; j < 8; )
			////    {
			////        for (j = 0; j < 8; j++)
			////        {
			////            if (ass[j] == -1) { ass[j] = 1; break; }
			////            else { ass[j] = -1; continue; }
			////        }

			////        int c = 0;
			////        for (int k = 0; k < 8; k++)
			////            if (ass[k] == 1) c++;

			////        bool evaluateCNF = cnf.Evaluate(ass);
			////        if (evaluateCNF != (c == 4))
			////        {
			////            throw new Exception();
			////        }
			////    }
			////    #endregion

			////    Console.ReadLine();

				
			////}









			////while (true)
			////{
			////    Console.Write(">>> ");
			////    string f = Console.ReadLine();
			////    var cnf = new Sentence(testWorld, f).BicondEliminate().ImplEliminate().DeMorgan().ConvertToCNF();
			////    var cnf2 = (CNFSentence)cnf.Clone();
			////    cnf.Compact();
			////    if (!cnf.IsEquivalentTo(cnf2)) throw new Exception();
			////    Console.WriteLine(cnf2);
			////    Console.WriteLine(cnf);

			////    Console.WriteLine();
			////}

			////    Func<int[], bool> fun = x => cnf.Evaluate(x);
			////    Console.WriteLine(CNFSentence.FromTruthTable(testWorld, fun, 3));
				
			////    //SATSolver s = new SATSolver();
			////    //int[] result = s.Solve(cnf);
			////    //if (result == null)
			////    //    Console.WriteLine("No solution");
			////    //else
			////    //{
			////    //    if (!s.CheckSolution(cnf, result))
			////    //    {
			////    //    }
			////    //    for (int i = 0; i < result.Length; i++)
			////    //    {
			////    //        Console.WriteLine(testWorld.Symbols[i] + " > " + (result[i] == 1 ? "True" : (result[i] == -1 ? "False" : "Any")));
			////    //    }
			////    //}
			////}

			//LogicalSystem testWorld = new LogicalSystem(Enumerable.Range(0, 20).Select(x => x.ToString()).ToArray());

			//while (true)
			//{
			//    Random rand = new Random();
			//    List<List<int>> formula = new List<List<int>>();
			//    for (int i = 0; i < 150; i++)
			//    {
			//        List<int> clause = new List<int>();
			//        for (int j = 0; j < 3; j++)
			//        {
			//            int v = rand.Next(testWorld.Symbols.Count);
			//            if (rand.NextDouble() < 0.5)
			//                v = ~v;
			//            clause.Add(v);
			//        }
			//        formula.Add(clause);
			//    }

			//    CNFSentence test3CNF = new CNFSentence(testWorld, formula);
			//    var original = (CNFSentence)test3CNF.Clone();
			//    test3CNF.Compact();

			//    if (!original.IsEquivalentTo(test3CNF)) throw new Exception();
			////    SATSolver solv = new SATSolver();
			////    int[] res = solv.Solve(test3CNF);
			////    Console.WriteLine("Nodes: " + solv.NodesExpanded);


			////    if (res == null)
			////        Console.WriteLine("No solution");
			////    else
			////    {
			////        if (!solv.CheckSolution(test3CNF, res))
			////        {
			////            throw new Exception();
			////        }
					
			////        for (int i = 0; i < res.Length; i++)
			////        {
			////            Console.WriteLine(testWorld.Symbols[i] + " > " + (res[i] == 1 ? "True" : (res[i] == -1 ? "False" : "Any")));
			////        }
			////    }

			//    Console.ReadLine();
			//}
		#endregion
	}
}
